Nuprl Lemma : no_repeats_l_index
11,40
postcript
pdf
T
:Type,
eq
:EqDecider(
T
),
L
:(
T
List),
i
:{0..||
L
||
}. no_repeats(
T
;
L
)
(index(
L
;
L
[
i
]) ~
i
)
latex
Definitions
t
T
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
SQType(
T
)
,
,
||
as
||
,
s
~
t
,
False
,
A
,
P
&
Q
,
A
B
,
i
j
<
k
,
{
x
:
A
|
B
(
x
)}
,
{
i
..
j
}
,
Type
,
EqDecider(
T
)
,
type
List
,
#$n
,
no_repeats(
T
;
l
)
,
l
[
i
]
,
index(
L
;
x
)
,
,
s
=
t
Lemmas
no
repeats
wf
,
int
seg
wf
,
length
wf1
,
deq
wf
,
no
repeats
mu
index
origin
T:Type, eq:EqDecider(T), L:(T List), i:{0..||L||
}. no_repeats(T;L) 
(index(L;L[i]) ~ i) T:Type, eq:EqDecider(T), L:(T List), i:{0..||L||}. no_repeats(T;L) (index(L;L[i]) ~ i) 
T Qx:A. B(x)
A
B j < k}